Nuprl Definition : frame-p
0,22
postcript
pdf
@
i
only events in
L
change
x
:
T
== vartype(
i
;
x
)
T
&
e
@
i
.
(kind(
e
)
L
)
(
x
after
e
) = (
x
when
e
)
latex
clarification:
frame-p(
es
;
i
;
T
;
x
;
L
)
== es-vartype(
es
;
i
;
x
)
T
==
& alle-at(
es
;
i
;
e
.
(es-kind(
es
;
e
)
L
Knd)
es-after(
es
;
x
;
e
) = es-when(
es
;
x
;
e
)
T
)
latex
Definitions
A
&
B
,
vartype(
i
;
x
)
,
e
@
i
.
P
(
e
)
,
P
Q
,
A
,
(
x
l
)
,
kind(
e
)
,
Knd
,
s
=
t
,
(
x
after
e
)
,
x
when
e
FDL editor aliases
frame-p
origin